Problem: norm(nil()) -> 0() norm(g(x,y)) -> s(norm(x)) f(x,nil()) -> g(nil(),x) f(x,g(y,z)) -> g(f(x,y),z) rem(nil(),y) -> nil() rem(g(x,y),0()) -> g(x,y) rem(g(x,y),s(z)) -> rem(x,z) Proof: Bounds Processor: bound: 1 enrichment: match automaton: final states: {7,6,5} transitions: rem1(3,1) -> 7* rem1(3,3) -> 7* rem1(4,2) -> 7* rem1(4,4) -> 7* rem1(1,2) -> 7* rem1(1,4) -> 7* rem1(2,1) -> 7* rem1(2,3) -> 7* rem1(3,2) -> 7* rem1(3,4) -> 7* rem1(4,1) -> 7* rem1(4,3) -> 7* rem1(1,1) -> 7* rem1(1,3) -> 7* rem1(2,2) -> 7* rem1(2,4) -> 7* g1(3,1) -> 7* g1(3,3) -> 7* g1(4,2) -> 7* g1(4,4) -> 7* g1(10,1) -> 10,6 g1(10,3) -> 10,6 g1(1,2) -> 7* g1(1,4) -> 7* g1(7,1) -> 10* g1(2,1) -> 7* g1(7,3) -> 10* g1(2,3) -> 7* g1(3,2) -> 7* g1(3,4) -> 7* g1(4,1) -> 7* g1(4,3) -> 7* g1(10,2) -> 10,6 g1(10,4) -> 10,6 g1(1,1) -> 7* g1(1,3) -> 7* g1(7,2) -> 10* g1(2,2) -> 7* g1(7,4) -> 10* g1(2,4) -> 7* nil1() -> 7,10 f1(3,1) -> 10* f1(3,3) -> 10* f1(4,2) -> 10* f1(4,4) -> 10* f1(1,2) -> 10* f1(1,4) -> 10* f1(2,1) -> 10* f1(2,3) -> 10* f1(3,2) -> 10* f1(3,4) -> 10* f1(4,1) -> 10* f1(4,3) -> 10* f1(1,1) -> 10* f1(1,3) -> 10* f1(2,2) -> 10* f1(2,4) -> 10* s1(8) -> 8,5 norm1(2) -> 8* norm1(4) -> 8* norm1(1) -> 8* norm1(3) -> 8* 01() -> 8,5 norm0(2) -> 5* norm0(4) -> 5* norm0(1) -> 5* norm0(3) -> 5* nil0() -> 1* 00() -> 2* g0(3,1) -> 3* g0(3,3) -> 3* g0(4,2) -> 3* g0(4,4) -> 3* g0(1,2) -> 3* g0(1,4) -> 3* g0(2,1) -> 3* g0(2,3) -> 3* g0(3,2) -> 3* g0(3,4) -> 3* g0(4,1) -> 3* g0(4,3) -> 3* g0(1,1) -> 3* g0(1,3) -> 3* g0(2,2) -> 3* g0(2,4) -> 3* s0(2) -> 4* s0(4) -> 4* s0(1) -> 4* s0(3) -> 4* f0(3,1) -> 6* f0(3,3) -> 6* f0(4,2) -> 6* f0(4,4) -> 6* f0(1,2) -> 6* f0(1,4) -> 6* f0(2,1) -> 6* f0(2,3) -> 6* f0(3,2) -> 6* f0(3,4) -> 6* f0(4,1) -> 6* f0(4,3) -> 6* f0(1,1) -> 6* f0(1,3) -> 6* f0(2,2) -> 6* f0(2,4) -> 6* rem0(3,1) -> 7* rem0(3,3) -> 7* rem0(4,2) -> 7* rem0(4,4) -> 7* rem0(1,2) -> 7* rem0(1,4) -> 7* rem0(2,1) -> 7* rem0(2,3) -> 7* rem0(3,2) -> 7* rem0(3,4) -> 7* rem0(4,1) -> 7* rem0(4,3) -> 7* rem0(1,1) -> 7* rem0(1,3) -> 7* rem0(2,2) -> 7* rem0(2,4) -> 7* problem: Qed